Termination w.r.t. Q proof of /tmp/tmp2XwMeo/t004.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

f(s(x)) → s(f(f(p(s(x)))))
f(0) → 0
p(s(x)) → x

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

f(s(x)) → s(f(f(p(s(x)))))
f(0) → 0
p(s(x)) → x

Q is empty.

The TRS is overlay and locally confluent. By [19] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

f(s(x)) → s(f(f(p(s(x)))))
f(0) → 0
p(s(x)) → x

The set Q consists of the following terms:

f(s(x0))
f(0)
p(s(x0))

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

F(s(x)) → F(f(p(s(x))))
F(s(x)) → F(p(s(x)))
F(s(x)) → P(s(x))

The TRS R consists of the following rules:

f(s(x)) → s(f(f(p(s(x)))))
f(0) → 0
p(s(x)) → x

The set Q consists of the following terms:

f(s(x0))
f(0)
p(s(x0))

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

F(s(x)) → F(f(p(s(x))))
F(s(x)) → F(p(s(x)))
F(s(x)) → P(s(x))

The TRS R consists of the following rules:

f(s(x)) → s(f(f(p(s(x)))))
f(0) → 0
p(s(x)) → x

The set Q consists of the following terms:

f(s(x0))
f(0)
p(s(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ MNOCProof

              ↳ Rewriting

  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

F(s(x)) → F(f(p(s(x))))
F(s(x)) → F(p(s(x)))

The TRS R consists of the following rules:

f(s(x)) → s(f(f(p(s(x)))))
f(0) → 0
p(s(x)) → x

The set Q consists of the following terms:

f(s(x0))
f(0)
p(s(x0))

We have to consider all minimal (P,Q,R)-chains.
We use the modular non-overlap check [17] to decrease Q to the empty set.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ MNOCProof

                ↳ QDP

              ↳ Rewriting

  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

F(s(x)) → F(f(p(s(x))))
F(s(x)) → F(p(s(x)))

The TRS R consists of the following rules:

f(s(x)) → s(f(f(p(s(x)))))
f(0) → 0
p(s(x)) → x

Q is empty.
We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule F(s(x)) → F(p(s(x))) at position [0] we obtained the following new rules:

F(s(x)) → F(x)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ MNOCProof

              ↳ Rewriting

                ↳ QDP

                  ↳ Rewriting

  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

F(s(x)) → F(f(p(s(x))))
F(s(x)) → F(x)

The TRS R consists of the following rules:

f(s(x)) → s(f(f(p(s(x)))))
f(0) → 0
p(s(x)) → x

The set Q consists of the following terms:

f(s(x0))
f(0)
p(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(s(x)) → F(f(p(s(x)))) at position [0,0] we obtained the following new rules:

F(s(x)) → F(f(x))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ MNOCProof

              ↳ Rewriting

                ↳ QDP

                  ↳ Rewriting

                    ↳ QDP

  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

F(s(x)) → F(x)
F(s(x)) → F(f(x))

The TRS R consists of the following rules:

f(s(x)) → s(f(f(p(s(x)))))
f(0) → 0
p(s(x)) → x

The set Q consists of the following terms:

f(s(x0))
f(0)
p(s(x0))

We have to consider all minimal (P,Q,R)-chains.
We have reversed the following QTRS:
The set of rules R is

f(s(x)) → s(f(f(p(s(x)))))
f(0) → 0
p(s(x)) → x

The set Q is empty.
We have obtained the following QTRS:

s(f(x)) → s(p(f(f(s(x)))))
0'(f(x)) → 0'(x)
s(p(x)) → x

The set Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

  ↳ QTRS Reverse

    ↳ QTRS

      ↳ RFCMatchBoundsTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

s(f(x)) → s(p(f(f(s(x)))))
0'(f(x)) → 0'(x)
s(p(x)) → x

Q is empty.

Termination of the TRS R could be shown with a Match Bound [6,7] of 2. This implies Q-termination of R.
The following rules were used to construct the certificate:

s(f(x)) → s(p(f(f(s(x)))))
0'(f(x)) → 0'(x)
s(p(x)) → x

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

130, 131, 132, 133, 135, 134, 136, 137, 139, 138

Node 130 is start node and node 131 is final node.

Those nodes are connect through the following edges:

130 to 131 labelled p_1(0), 0'_1(0), f_1(0), s_1(0), p_1(1), f_1(1), s_1(1), 0'_1(1)
130 to 132 labelled s_1(0)
130 to 136 labelled s_1(1)
130 to 134 labelled f_1(1)
130 to 138 labelled f_1(2)
131 to 131 labelled #_1(0)
132 to 133 labelled p_1(0)
133 to 134 labelled f_1(0)
135 to 131 labelled s_1(0), p_1(1), f_1(1), s_1(1), 0'_1(1)
135 to 136 labelled s_1(1)
135 to 138 labelled f_1(2)
134 to 135 labelled f_1(0)
136 to 137 labelled p_1(1)
137 to 138 labelled f_1(1)
139 to 131 labelled s_1(1), p_1(1), f_1(1), 0'_1(1)
139 to 136 labelled s_1(1)
139 to 138 labelled f_1(2)
138 to 139 labelled f_1(1)